Теорема о полноте метода резолюций

КНФ $F = C_{1} \land \dots \land C_{k}$ является противоречием $\iff$ существует доказательство методом резолюций с условиями $C_{1}, \dots, C_{k}$ и заключением $\square$.

$\Large{\impliedby}$ (Корректность) Рассмотрим доказательство методом резолюций с заключением $\square$. Каждая формула в нем либо является условием, либо получена из предыдущих по правилу резолюций. Согласно лемме, результат применения правила резолюций является следствием посылок. В силу транзитивности отношения «быть следствием», любая формула в доказательстве является следствием $F$. Пустой клоз $\square$ (константа 0) является следствием формулы $x \land \bar{x}$, следовательно, $0$ — следствие $F$. Это означает, что $F \implies 0$, то есть $F$ — противоречие. $\Large{\implies}$ (Полнота) Проведем индукцию по числу $n$ переменных в $F$. **База индукции**: $n=1$. Если $F$ — противоречие, то $F$ содержит клозы $x$ и $\bar{x}$. По правилу резолюций из них выводится пустой клоз $\square$. **Шаг индукции**: Пусть утверждение верно для $n-1$ переменных. Пусть $F = F(x_{1}, \dots, x_{n})$ и $S = \{C_{1}, \dots, C_{k}\}$ — множество клозов. Построим множества клозов $S^{+}$ и $S^{-}$: $$S^{+} = \{C \in S \mid x_{n} \notin C\} \cup \{C \mid (C \lor x_{n}) \in S\}$$ $$S^{-} = \{C \in S \mid x_{n} \notin C\} \cup \{C \mid (C \lor \bar{x}_{n}) \in S\}$$ $F^{+} = \bigwedge_{C \in S^{+}} C$ является противоречием (иначе, если существует набор, выполняющий $F^{+}$, добавив к нему $x_{n}=0$, мы бы получили набор, выполняющий $F$, что невозможно). Аналогично, $F^{-}$ — противоречие. По предположению индукции, из $S^{+}$ и $S^{-}$ можно вывести пустой клоз. Рассмотрим вывод пустого клоза из $S^{+}$. Если в нем участвовал клоз $C \in S^{+} \setminus S$, то в $S$ ему соответствует $(C \lor x_{n})$. Построив аналогичный вывод из $S$, мы добавим литерал $x_{n}$ ко всем следствиям таких клозов, и в результате вместо пустого клоза выведем $x_{n}$. Аналогично, из вывода пустого клоза из $S^{-}$ получим вывод $\bar{x}_{n}$ из $S$. Применив правило резолюции к полученным $x_{n}$ и $\bar{x}_{n}$, получим $\square$. $\square$